$\forall$$T$, $A$:Type, $f$:($A$$\rightarrow$$T$), $l$:IdLnk.
\\[0ex]Normal($A$)
\\[0ex]$\Rightarrow$ Normal($T$)
\\[0ex]$\Rightarrow$ send\_onceR\{done:ut2, tg:ut2, b:ut2, done1:ut2\}($T$; $A$; $f$; $l$) $\in$ Realizer